The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) Berlin, March 25–29, 1985 Volume 1: Colloquium on Trees in Algebra and Programming (CAAP' 85)
Stream-processing functions provide an excellent semantic model for the abstract representation of systems of nondeterministic concurrent communicating agents. Based on this model a formalism for the specification of such functions is suggested. This way a fully modular, compositional methodology for the specification and the design of distributed systems and their components is derived. Concepts...
Requirements of specification languages for distributed systems are considered, and a two level approach based on a kernel metalanguage and many application-oriented extensions is advocated. The method is applied to some models developed by the authors, organized in a tree-like refinement structure.
It is one of our fundamental theses that major improvements in software engineering practice will come about only through the development and use of software development tools. This thesis is based on our belief that formal methods will ultimately have a far more profound effect on software engineering productivity than management based methods, programming language design, or fast hardware. But we...
The software crisis results from our disorderly concepts of "program". These make programming an art, rather than an engineering discipline. Such a discipline would at least require that we have stocks of useful off-the-shelf programs and collections of standard theorems that can be applied repeatedly. We have neither. Mathematical systems are often distinguished by a set of operations...
We examine three disparate views of the type structure of programming languages: Milner's type deduction system and polymorphic let construct, the theory of subtypes and generic operators, and the polymorphic or second-order typed lambda calculus. These approaches are illustrated with a functional language including product, sum and list constructors. The syntactic behavior of types is formalized...
In this paper we prove a conjecture of Erdös and Palka on the maximum size of random trees. Furthermore, while, generally speaking, in the probabilistic analysis the results are proved only when the size of the graphs tends to infinity, in this case, with extremely small probability of error, the results also hold for graphs of small size.
This paper generalizes the multidimensional searching scheme of Dobkin and Lipton [SIAM J. Comput. 5(2), pp. 181–186, 1976] for the case of arbitrary (as opposed to linear) real algebraic varieties. Let d,r be two positive constants and let P1,...,Pn be n rational r-variate polynomials of degree ≤d. Our main result is an $$O(n^{2^{r + 6} } )$$ ...
The subject of the paper is the connection between the typed λ-calculus and the cartesian closed categories, pointed out by several authors. Three languages and their theories, defined by equations, are shown to be equivalent: the typed λc-calculus (i.e. the λ-calculus with explicit products and projections) λcK, the free cartesian closed category CCC ...
A new partial ordering scheme for proving uniform termination of term rewriting systems is presented. The basic idea is that two terms are compared by comparing the paths through them. It is shown that the ordering is a well-founded simplification ordering and also a strict extension of the recursive path ordering scheme of Dershowitz. Terms can be compared under this path ordering in polynomial time.
An approach for synthesizing data type implementations based on the theory of term rewriting systems is presented. A specification is assumed to be given as a system of equations; an implementation is derived from the specification as another system of equations. The proof based approach used for the synthesis consists of reversing the process of proving theorems (i.e. searching for appropriate theorems...
In this paper we show that the notion of bisimulation for a class of labelled transition systems (the class of nondeterministic processes) may be restated as one of “reducibility to a same system” via a simple reduction relation. The reduction relation is proven to enjoy some desirable properties, notably a Church-Rosser property. We also show that, when restricted to finite nondeterministic processes,...
We address the problem of characterizing fair (infinite) behaviours of concurrent systems as limits of finite approximations. The framework chosen is Milner's Calculus of Communicating Systems. The results can be summarized as follows. On the set FD of all finite derivations in the calculus we define three distances: da, dw, ds. Then the metric completion of (FD,da) yields the space of all derivations,...
Logical proof systems for concurrent programs are notoriously complex, often involving arbitrary restrictions. One of the main reasons for this is that unlike other major programming concepts parallelism does not appear to have a logical correlate. Here using a simple semantic strategy we tentatively propose one and offer an example modal proof system for a subset of Milner's SCCS. The proof rules...
In the present paper we generalize the well-known PARALLELISM THEOREM for graph derivations to the AMALGAMATION THEOREM. In this theorem the assumption of ‘parallel independence’ is dropped. For each pair of productions together with a relational production (allowing productions to be associated with each other) we construct a single ‘amalgamated’ production. The AMALGAMATION THEOREM states that graph...
Decompilation denotes the translation from lower level into higher level programming languages. Here we deal with the aspect of detecting higher level control structures, including loops with any number of exits, in line-oriented programs. The detection is carried out on the control flow graph of the source program by means of so called wellstructuring transformations. We show that the iteration...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.